Nuprl Definition : es_realizer_ind_Rplus_compseq_tag_def 0,22

es_realizer_ind_Rplus{es realizer ind Rplus compseq tag def:ObjectId}
es_realizer_ind_Rplus(v11,v12,v13.rframe(v11;v12;v13);
es_realizer_ind_Rplus(v21,v22,v23.bframe(v21;v22;v23);
es_realizer_ind_Rplus(v31,v32,v33.aframe(v31;v32;v33);
es_realizer_ind_Rplus(v41,v42,v43,v44,v45.pre(v41;v42;v43;v44;v45);
es_realizer_ind_Rplus(v51,v52,v53,v54,v55,v56.sends(v51;v52;v53;v54;v55;v56);
es_realizer_ind_Rplus(v61,v62,v63,v64,v65,v66.effect(v61;v62;v63;v64;v65;v66);
es_realizer_ind_Rplus(v71,v72,v73.sframe(v71;v72;v73);
es_realizer_ind_Rplus(v81,v82,v83,v84.frame(v81;v82;v83;v84);
es_realizer_ind_Rplus(v91,v92,v93,v94.init(v91;v92;v93;v94);
es_realizer_ind_Rplus(v101,v102,v103,v104.plus(v101;v102;v103;v104);
es_realizer_ind_Rplus(none;
es_realizer_ind_Rplus(right;
es_realizer_ind_Rplus(left)
== compseq(case left  right of 
== compseq(Rnone => none
== compseq(Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
== compseq(Rinit(loc,T,x,v)=> init(loc;T;x;v)
== compseq(Rframe(loc,T,x,L)=> frame(loc;T;x;L)
== compseq(Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
== compseq(Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
== compseq(Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
== compseq(Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
== compseq(Raframe(loc,k,L)=> aframe(loc;k;L)
== compseq(Rbframe(loc,k,L)=> bframe(loc;k;L)
== compseq(Rrframe(loc,x,L)=> rframe(loc;x;L);
== compseq(plus(left
== compseq(plus;right
== compseq(plus;case left of 
== compseq(plus;Rnone => none
== compseq(plus;Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
== compseq(plus;Rinit(loc,T,x,v)=> init(loc;T;x;v)
== compseq(plus;Rframe(loc,T,x,L)=> frame(loc;T;x;L)
== compseq(plus;Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
== compseq(plus;Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
== compseq(plus;Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
== compseq(plus;Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
== compseq(plus;Raframe(loc,k,L)=> aframe(loc;k;L)
== compseq(plus;Rbframe(loc,k,L)=> bframe(loc;k;L)
== compseq(plus;Rrframe(loc,x,L)=> rframe(loc;x;L)
== compseq(plus;case right of 
== compseq(plus;Rnone => none
== compseq(plus;Rplus(left,right)=>rec1,rec2.plus(left;right;rec1;rec2)
== compseq(plus;Rinit(loc,T,x,v)=> init(loc;T;x;v)
== compseq(plus;Rframe(loc,T,x,L)=> frame(loc;T;x;L)
== compseq(plus;Rsframe(lnk,tag,L)=> sframe(lnk;tag;L)
== compseq(plus;Reffect(loc,ds,knd,T,x,f)=> effect(loc;ds;knd;T;x;f)
== compseq(plus;Rsends(ds,knd,T,l,dt,g)=> sends(ds;knd;T;l;dt;g)
== compseq(plus;Rpre(loc,ds,a,T,P)=> pre(loc;ds;a;T;P)
== compseq(plus;Raframe(loc,k,L)=> aframe(loc;k;L)
== compseq(plus;Rbframe(loc,k,L)=> bframe(loc;k;L)
== compseq(plus;Rrframe(loc,x,L)=> rframe(loc;x;L))) 
latex


Definitionsleft  right, es realizer ind

origin